COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00025 ENDMK
C⊗;

to write unify(x,y) where x and y are sequences containing variables, constants
or functional terms. The mgu is returned if x and y are unifable; the mgu is 
either empty or a sequence of pairs (of substitutions), such that application
of the substitutions to x and y results in identical expressions; if x and y
are not unifiable the  atom LOSE is returned.


want double  loop on x and y.


istermseq(x)∧istermseq(y)
    {A;R; while ¬empty[x]∧ ¬empty[y] do B;x←rest[x]; y← rest[y]}
(z=LOSE∧ ¬unifiable(x,y))∨mgunified(z,x,y)

using V4 machine should generate:


istermseq(x)∧istermseq(y){A}R; 
R∧(¬empty[x]∧¬empty[y]){B;x←rest[x]; y←rest[y]}R 
R∧¬(¬empty[x]∧¬empty[y])⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)
-------------------------------------------
istermseq(x)∧istermseq(y)
    {A;R; while ¬empty[x]∧ ¬empty[y] do B;x←rest[x]; y← rest[y]}
(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)

and expand it (using V1) to:

istermseq(x)∧istermseq(y){A}R(x,y); 
R(x,y)∧(¬empty[x]∧¬empty[y]){B}R(rest[x],rest[y]);
R(x,y)∧¬(¬empty[x]∧¬empty[y])⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)
-------------------------------------------
istermseq(x)∧istermseq(y)
    {A;R(x,y); while ¬empty[x]∧ ¬empty[y] do B;x←rest[x]; y← rest[y]}
(z=LOSE∧ ¬unifible(x,y))∨ mgunified(z,x,y)



woops! want new variable to contain substitution being built.
want z←NIL followed by loop. machine regroups and does:

istermseq(x)∧istermseq(y){z←()}R(x,y,z);    				 (1)
R(x,y,z)∧(¬empty[x]∧¬empty[y]){B}R(rest[x],rest[y],z);			 (2)
R(x,y,z)∧¬(¬empty[x]∧¬empty[y])⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)(3)
-------------------------------------------
istermseq(x)∧istermseq(y)
    {z←();R(x,y,z); while ¬empty[x]∧ ¬empty[y] do B;x←rest[x]; y← rest[y]}
(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)


Since (3) above is a put implication, perhaps we should attempt to 
specify the invariant, R.

Well it's that z applied to the initial segments of x and y unify them.
So our loop must save  the inputs say in x0 and y0.

Not necessarily: it is only to initial segments  of the inputs which are
of interest.

Observation: at first glance the easiest way to specify invariant
is in terms of two variables say x1, and y1 which contain the initial segments
of x and y and are constructed during the program(by concat). The ONLY reason
for having x1 and y1 is for assertions. Then besides assertions being added
to program we might also add program.(later I was told that this hack is called
virtual program)

So:
istermseq(x)∧istermseq(y)∧istermseq(x1)∧istermseq(y1)∧(issub(z)∨z=LOSE)
	{x1←();y1←();z←()}
 	R(x,x1,y,y1,z)                   (1)
R(x,x1,y,y1,z)∧(¬empty[x]∧¬empty[y])
	{B;x1←concat[first[x];x1];y1← concat[first[y];y1]}
	R(rest[x],x1,rest[y],y1,z);			 (2)
R(x,x1,y,y1,z)∧¬(¬empty[x]∧¬empty[y])⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)(3)
-------------------------------------------
istermseq(x)∧istermseq(y)∧istermseq(x1)∧istermseq(y1)∧(issub(z)∨z=LOSE)
    {x1←();
     y1←();
     z←();R(x,x1,y,y1,z); 
     while ¬empty[x]∧ ¬empty[y] do B;
     x1← concat[first[x];x1]; y1← concat[first[y];y1];
     x←rest[x]; y← rest[y]}
(z=LOSE∧ ¬unifiable(x,y))∨ unified(z,x,y)

Things are getting complicated, but are still manageable. We should 
finish off the invariant.

Using V1 and V3 we can simplfy (1):
istermseq(x)∧istermseq(y)∧istermseq(x1)∧istermseq(y1)∧(issub(z)∨z=LOSE)
	⊃
 	R(x,(),y,(),())                  (1)

Similarly using V1 on (2):
R(x,x1,y,y1,z)∧(¬empty[x]∧¬empty[y])
	{B}
	R(rest[x],concat[first[x];x1],rest[y],concat[first[y];y1],z); (2)

also (3) will simplify slightly:
R(x,x1,y,y1,z)∧¬(¬empty[x]∧¬empty[y])⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)


So let us pick R(x,x1,y,y1,z) as:
istermseq(x)∧istermseq(y)∧istermseq(x1)∧istermseq(y1)∧(issub(z)
∧.... 
** troubles, time to regroup. We wish to say that append[x1;x] is the original
** termlist, but we can't since termlist is being destroyed.
** so we must save it. Similarly for y. We use x2 and y2 for destruction.


istermseq(x)∧istermseq(y)
 ∧istermseq(x1)∧istermseq(y1)∧
 ∧istermseq(x2)∧istermseq(y2)∧(issub(z)∨z=LOSE)
	{x1←();y1←();x2←x;y2←y;z←()}
 	R(x,x1,x2,y,y1,y2,z)                   (1)
R(x,x1,x2,y,y1,y2,z)∧(¬empty[x2]∧¬empty[y2])
	{B;x1←concat[first[x2];x1];y1← concat[first[y2];y1]}
	R(x,x1,rest[x2],y,y1,rest[y2],z);			 (2)
R(x,x1,x2,y,y1,y2,z)∧¬(¬empty[x2]∧¬empty[y2])⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)(3)
-------------------------------------------
istermseq(x)∧istermseq(y)
 ∧istermseq(x1)∧istermseq(y1)∧
 ∧istermseq(x2)∧istermseq(y2)∧(issub(z)∨z=LOSE)
    {x1←();
     x2←x;
     y1←();
     y2←y;
     z←();R(x,x1,x2,y,y1,y2,z); 
     while ¬empty[x2]∧ ¬empty[y2] do B;
     x1← concat[first[x2];x1]; y1← concat[first[y2];y1];
     x2←rest[x2]; y2← rest[y2]}
(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)

Now, back to R(x,x1,x2,y,y1,y2,z)
New (1) simplifies:

istermseq(x)∧istermseq(y)
 ∧istermseq(x1)∧istermseq(y1)∧
 ∧istermseq(x2)∧istermseq(y2)∧(issub(z)∨z=LOSE)
	⊃
 	R(x,(),x,y,(),y,())                  

So does (2):

R(x,x1,x2,y,y1,y2,z)∧(¬empty[x2]∧¬empty[y2])
	{B}
	R(x,concat[first[x2];x1],rest[x2],y,concat[first[y2];y1],rest[y2],z)

and a slightly simplified (3)
R(x,x1,x2,y,y1,y2,z)∧(empty[x2]∨empty[y2])
    ⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)

So try again for R(x,x1,x2,y,y1,y2,z):

istermseq(x)∧istermseq(y)
 ∧istermseq(x1)∧istermseq(y1)
 ∧istermseq(x2)∧istermseq(y2)
 ∧((issub(z)∧x=append[x1;x2]∧y=append[y1;y2]∧mgunified(z;x1;y1))
   ∨(z=LOSE∧¬unifiable(x,y)
   )


This R makes (1) true. (using properties of append and mgunified and issub
***make the properties explicit****


Look at (3):

R(x,x1,x2,y,y1,y2,z)∧(empty[x2]∨empty[y2])
    ⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)

istermseq(())∧istermseq(())
 ∧istermseq(x1)∧istermseq(y1)
 ∧istermseq(x2)∧istermseq(y2)
 ∧((issub(z)∧x=append[x1;()]∧y=append[y1;()]∧mgunified(z;x1;y1))
   ∨(z=LOSE∧¬unifiable(x,y)
   )
    ⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)

**mumble ok.**doit

now (2)
R(x,x1,x2,y,y1,y2,z)∧(¬empty[x2]∧¬empty[y2])
	{B}
	R(x,concat[first[x2];x1],rest[x2],y,concat[first[y2];y1],rest[y2],z)

Before going off to write {B} we should try to tighten up the
outer loops: namely there is no point to bother with {B} if z is LOSE.
So we wish to modify  the termination on "while" to exit if LOSE is
given to z as value.
This results in:

istermseq(x)∧istermseq(y)
 ∧istermseq(x1)∧istermseq(y1)∧
 ∧istermseq(x2)∧istermseq(y2)∧(issub(z)∨z=LOSE)
	⊃
 	R(x,(),x,y,(),y,())                  

R(x,x1,x2,y,y1,y2,z)∧(¬empty[x2]∧¬empty[y2]∧¬z=LOSE)
	{B}
	R(x,concat[first[x2];x1],rest[x2],y,concat[first[y2];y1],rest[y2],z)

R(x,x1,x2,y,y1,y2,z)∧(empty[x2]∨empty[y2]∨z=LOSE)
    ⊃(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)
_________________________________________________________
istermseq(x)∧istermseq(y)
 ∧istermseq(x1)∧istermseq(y1)∧
 ∧istermseq(x2)∧istermseq(y2)∧(issub(z)∨z=LOSE)
    {x1←();
     x2←x;
     y1←();
     y2←y;
     z←();R(x,x1,x2,y,y1,y2,z); 
     while ¬empty[x2]∧ ¬empty[y2]∧¬z=LOSE do B;
     x1← concat[first[x2];x1]; y1← concat[first[y2];y1];
     x2←rest[x2]; y2← rest[y2]}
(z=LOSE∧ ¬unifiable(x,y))∨ mgunified(z,x,y)

Now we are in reasonable shape: the outer loops are coded and
the inner  structure, represented by "{B}" is isolated, its
I/O requirements are clear(?: we will see!!). Let's expand (2) using R

istermseq(x)∧istermseq(y)
 ∧istermseq(x1)∧istermseq(y1)
 ∧istermseq(x2)∧istermseq(y2)
 ∧((issub(z)∧x=append[x1;x2]∧y=append[y1;y2]∧mgunified(z;x1;y1))
   ∨(z=LOSE∧¬unifiable(x1,y1)
   )
∧(¬empty[x2]∧¬empty[y2] ∧¬z=LOSE)
     {B}

istermseq(x)∧istermseq(y)
 ∧istermseq(concat[first[x2];x1])∧istermseq(concat[first[y2];y1])
 ∧istermseq(rest[x2])∧istermseq(rest[y2])
 ∧((issub(z)∧x=append[concat[first[x2];x1];rest[x2]]
		∧y=append[concat[first[y2];y1];rest[y2]]
		     ∧mgunified(z;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(z=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

Simplifications are rampant( i.e. making assumptions "global;
properties of istermseq, etc.):

issub(z)∧x=append[x1;x2]∧y=append[y1;y2]∧mgunified(z;x1;y1)
     {B}
 ∧((issub(z)∧x=append[concat[first[x2];x1];rest[x2]]
		∧y=append[concat[first[y2];y1];rest[y2]]
		     ∧mgunified(z;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(z=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

Using properties of append and concat:
issub(z)∧mgunified(z;x1;y1)
     {B}
((issub(z)∧mgunified(z;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(z=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

Expand "{B}" to return new value of z, either  substitution unifying
first elements of x2 and y2 or returning LOSE if not possible:

issub(z)∧mgunified(z;x1;y1)
     {C;z←unify1[first[x2];first[y2];z]}
((issub(z)∧mgunified(z;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(z=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

By V1 gives:

issub(z)∧mgunified(z;x1;y1)
     {C}
((issub(unify1[first[x2];first[y2];z])
 ∧mgunified(unify1[first[x2];first[y2];z];concat[first[x2];x1];concat[first[y2];y1]))
   ∨(unify1[first[x2];first[y2];z]=LOSE
       ∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )


After unify1[x;y;z]:
 x is a term; y is a term; z is a substitution; 
isterm(x)∧isterm(y)∧issub(z)

if, after application of the substitution z, the transformed terms x and y
are unifiable, then we will return that necessary substitution. If unification
is not posible we return LOSE.




Try it: V8;
issub(z)∧isterm(x)∧isterm(y){z:unify1[x;y;z];A}issub(z)∧mgunif_term(x,y,compose **
****troubles: z before and after.
** decision: should we go in with substitutions already made?
** there is a related decision which we have to make: how to update the subsitution.
** this could give the following:

issub(z)∧mgunified(z;x1;y1)
     {C;z1←unify1[subst[first[x2];z];subst[first[y2];z]]
        if issub(z1) then z ← compose[z;z1] else z←LOSE}
((issub(z)∧mgunified(z;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(z=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

By V5 now:      (4)
issub(z)∧mgunified(z;x1;y1)
     {C;
      z1←unify1[subst[first[x2];z];subst[first[y2];z]]
      issub(z1)-IF; 
      z ← compose[z;z1];}
((issub(z)∧mgunified(z;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(z=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

and            (5)

issub(z)∧mgunified(z;x1;y1)
     {C;
      z1←unify1[subst[first[x2];z];subst[first[y2];z]]
      ¬issub(z1)-IF
       z← LOSE} 
((issub(z)∧mgunified(z;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(z=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

(5) is succeptible to V1;
issub(z)∧mgunified(z;x1;y1)
     {C;
      z1←unify1[subst[first[x2];z];subst[first[y2];z]]
      ¬issub(z1)-IF
      }
((issub(LOSE)∧mgunified(LOSE;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(LOSE=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

then use V3(iii):
issub(z)∧mgunified(z;x1;y1)
     {C;
      z1←unify1[subst[first[x2];z];subst[first[y2];z]]
      }
¬issub(z1) ⊃
((issub(LOSE)∧mgunified(LOSE;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(LOSE=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

Now V1:

issub(z)∧mgunified(z;x1;y1)
     {C;
      }
¬issub(unify1[subst[first[x2];z];subst[first[y2];z]])
⊃
((issub(LOSE)∧mgunified(LOSE;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(LOSE=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

Time to look at program's current state without assertions:
    {x1←();
     x2←x;
     y1←();
     y2←y;
     z←();R(x,x1,x2,y,y1,y2,z); 
     while ¬empty[x2]∧ ¬empty[y2]∧¬z=LOSE do 
      [|C;z1←unify1[subst[first[x2];z];subst[first[y2];z]]
          if issub(z1) then z ← compose[z;z1] else z←LOSE |]
     x1← concat[first[x2];x1]; y1← concat[first[y2];y1];
     x2←rest[x2]; y2← rest[y2]}

Looks reasonable: so we continue to thrash  (5).
{C} should be {NULL}.

issub(z)∧mgunified(z;x1;y1)
   ⊃
 (¬issub(unify1[subst[first[x2];z];subst[first[y2];z]])
      ⊃
    (¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

What about (4)? since "C" is empty we have:

issub(z)∧mgunified(z;x1;y1)
     {z1←unify1[subst[first[x2];z];subst[first[y2];z]]
      issub(z1)-IF; 
      z ← compose[z;z1];}
((issub(z)∧mgunified(z;concat[first[x2];x1];concat[first[y2];y1]))
   ∨(z=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

Using V1:

issub(z)∧mgunified(z;x1;y1)
     {z1←unify1[subst[first[x2];z];subst[first[y2];z]]
      issub(z1)-IF; 
      }
((issub(compose[z;z1])∧mgunified(compose[z;z1];concat[first[x2];x1];concat[first[y2];y1]))
   ∨(compose[z;z1]=LOSE∧¬unifiable(concat[first[x2];x1],concat[first[y2];y1])
   )

Using V3(iii) and properties of compose:
issub(z)∧mgunified(z;x1;y1)
     {z1←unify1[subst[first[x2];z];subst[first[y2];z]]
      }
issub(z1)
  ⊃
((issub(compose[z;z1])∧mgunified(compose[z;z1];concat[first[x2];x1];concat[first[y2];y1]))
   )

And with V1 and V3(i):

issub(z)∧mgunified(z;x1;y1)
 
 ⊃
    issub(unify1[subst[first[x2];z];subst[first[y2];z]])
       ⊃
     ((issub(compose[z; unify1[subst[first[x2];z];subst[first[y2];z]]])
         ∧mgunified(compose[z;unify1[subst[first[x2];z];subst[first[y2];z]]];
                    concat[first[x2];x1];
                    concat[first[y2];y1]))
      )

Simplification (assuming issub(z) and issub(unify1..)) and properties of
 compose)  yields:

mgunified(z;x1;y1) ⊃
          mgunified(compose[z;unify1[subst[first[x2];z];subst[first[y2];z]]];
                    concat[first[x2];x1];
                    concat[first[y2];y1])))


Now it seems reasonable to go after unify1[x;y] <= ... .

On entry we have: isterm(x) and isterm(y) 
On exit the value of unify1(x,y) is LOSE if  ¬unifiable(x,y) or 
                                 is a substitution which is the m.g.u. of x and y.


Too much pain is inflicted here in having to describe the dispatching
on data-types in terms of conditional expressions.
However...:

_____________________________________
isterm(x) and isterm(y) 
{if is_var(x) then B else C}
 LOSE if  ¬unifiable(x,y) or issub which is the m.g.u. of x and y.